$\forall$$T$:Type, $P$:($T$$\rightarrow\mathbb{P}$), $f$:($\forall$$x$:$T$. Dec($P$($x$))), $x$:$T$.
\\[0ex]($\uparrow$can{-}apply(p{-}co{-}filter($f$);$x$)) $\Rightarrow$ (do{-}apply(p{-}co{-}filter($f$);$x$) = $x$)